Nuprl Lemma : ma-valtype-subtype
11,40
postcript
pdf
k
:Knd,
da
,
da'
:
a
:Knd fp
Type.
da
da'
(Valtype(
da'
;
k
)
r Valtype(
da
;
k
))
latex
Definitions
x
:
A
.
B
(
x
)
,
P
Q
,
Valtype(
da
;
k
)
,
t
T
,
x
.
t
(
x
)
,
{
T
}
,
x
(
s
)
,
Lemmas
subtype-fpf-cap
,
Knd
wf
,
Kind-deq
wf
,
fpf-sub
wf
,
fpf
wf
origin
k:Knd, da, da':a:Knd fp
Type. da 
da' 
(Valtype(da';k) r Valtype(da;k)) k:Knd, da, da':a:Knd fp Type. da da' (Valtype(da';k) r Valtype(da;k)) x:A. B(x) Q
T
x. t(x)